package probsym.heap;
import gov.nasa.jpf.symbc.Debug;
import gov.nasa.jpf.symbc.probsym.Analyze;


public class ExSymExeHeap {

	static class Node  {
		//@Symbolic("true")
		int elem;

		//Symbolic("true")
		Node next;


		  /* we want to let the user specify that this method should be symbolic */
		/*
		  Node swapNode() {

		  if(next!=null)
			  if(elem > next.elem) {
				  elem = 0;
				  Node t = next;
				  next = t.next;
				  t.next = this;
				  return t;
			  }
		  return this;
		  }
		*/  
		
		Node createNode() {
			return next;
		}
		
		  Node swapNode() {
			  //next = this;
			  if (next != this) {
				  System.out.println("NO!");
			  }
			  else {
				  System.out.println("Yes");
			  }
			  next = this;
			  if (next != this) {
				  System.out.println("NO! 2");
			  }
			  else {
				  System.out.println("Yes 2");
			  }
			  return this;
		  }
		  
	}


  public static void main (String[] args) {

	  Node n = new Node();
	  Node m = new Node();
	  n =  (Node) Debug.makeSymbolicRef("sym_n", n);
	  Debug.printHeapPC("0 HeapPC: ");	  
	  m =  (Node) Debug.makeSymbolicRef("input_m", m);
	  Debug.printHeapPC("1 HeapPC: ");
	  Debug.printSymbolicRef(n,"node = ");	  
	  
	  if (m == n) {
		  Debug.printHeapPC("5 HeapPC: ");
	  }
	  else {
		  Debug.printHeapPC("6 HeapPC: ");
	  }
	  
      if (n != null)
    	 m = n.createNode();
      Analyze.coverage(""+1);
//	  Node m = new Node();
//	  n =  (Node) Debug.makeSymbolicRef("input_n", n);
//	  if (n !=null)
//		  m = n.swapNode();
	  Debug.printHeapPC("2 HeapPC: ");
	  Debug.printPC("PC: ");
	  Debug.printSymbolicRef(m,"return:");
	  System.out.println("*****************");
  }

}

